/LMAR=0/XLINE=3/FONT#0=BAXL30[FNT,CLT]/FONT#1=BAXM30/FONT#2=BAXB30[FNT,CLT]/FONT#5=GACS25/FONT#3=SUB/FONT#4=SUP/FONT#7=SYMB30[FNT,CLT]

␈↓ ↓H␈↓␈↓ ∧+COMPUTER SCIENCE DEPARTMENT
␈↓ ↓H␈↓␈↓ ¬πSTANFORD UNIVERSITY
␈↓ ↓H␈↓CS206  ␈↓ βiRECURSIVE PROGRAMMING AND PROVING ␈↓ 
0FALL 1979

␈↓ ↓H␈↓α␈↓ ¬FTERM PROJECTS

␈↓ ↓H␈↓        A␈αterm␈αproject␈αis␈αnot␈αrequired␈αin␈αorder␈αto␈αpass␈αCS206␈αor␈αeven␈αto␈αget␈αa␈αgrade␈αof␈αB␈αif␈αyour
␈↓ ↓H␈↓homework␈α
and␈α
exams␈αare␈α
good␈α
enough.␈α However,␈α
if␈α
you␈α
wish␈αto␈α
get␈α
some␈αflavor␈α
of␈α
A␈αthen␈α
doing
␈↓ ↓H␈↓a␈αgood␈α
term␈αproject␈αis␈α
necessary.␈α Term␈α
projects␈αwill␈αbe␈α
due␈αon␈α
the␈αday␈αof␈α
the␈αfinal␈α
exam.␈α Any
␈↓ ↓H␈↓term project turned in ahead of time will be likely to get a more thorough reading.

␈↓ ↓H␈↓        The␈αterm␈αproject␈αis␈αyour␈αopportunity␈αto␈αdirect␈αyour␈αattention␈αto␈αand␈αget␈αexperience␈αin␈αsome
␈↓ ↓H␈↓area␈α
that␈α
interests␈αyou.␈α
  Briefly␈α
the␈αpossibilities␈α
include␈α
writing␈αand␈α
documenting␈α
an␈αsubstantial
␈↓ ↓H␈↓LISP␈α∀program,␈α∀proving␈α∃the␈α∀correctness␈α∀of␈α∀a␈α∃moderate␈α∀sized␈α∀LISP␈α∀program,␈α∃or␈α∀developing
␈↓ ↓H␈↓techniques and principles for proving properties for some class of programs.

␈↓ ↓H␈↓        The␈α
write␈α
up␈α
of␈α
your␈α
project␈α
is␈α
the␈α
main␈α
thing␈α
that␈α
will␈α
get␈α
graded␈α
so␈α
it␈α
should␈α
be␈α
clear␈α
and
␈↓ ↓H␈↓carefully␈α∂done.␈α∂ It␈α∂should␈α∂include␈α∞a␈α∂brief␈α∂description␈α∂of␈α∂what␈α∂you␈α∞set␈α∂out␈α∂to␈α∂do␈α∂and␈α∂what␈α∞you
␈↓ ↓H␈↓accomplished.␈α∞ If␈α∞you␈α
write␈α∞a␈α∞progam,␈α
you␈α∞should␈α∞give␈α
a␈α∞description␈α∞of␈α
how␈α∞it␈α∞works␈α∞and␈α
why,
␈↓ ↓H␈↓including␈α∞a␈α∞description␈α∂of␈α∞the␈α∞data␈α∂structures␈α∞it␈α∞is␈α∂acting␈α∞on␈α∞and␈α∂the␈α∞basic␈α∞operations␈α∂on␈α∞these
␈↓ ↓H␈↓structures.␈α∂ The␈α∂code␈α∂for␈α∂the␈α∂program␈α∂should␈α∂be␈α∂included␈α∂with␈α∂brief␈α∂comments␈α∂in␈α∂appropriate
␈↓ ↓H␈↓places to guide the reader.  Some sample runs should also be included.

␈↓ ↓H␈↓        The␈α∞following␈α∞are␈α
some␈α∞ideas␈α∞for␈α∞term␈α
projects.␈α∞ You␈α∞may␈α∞choose␈α
one␈α∞of␈α∞these,␈α∞or␈α
design
␈↓ ↓H␈↓your own project.


␈↓ ↓H␈↓αProving

␈↓ ↓H␈↓1.␈α
Develop␈α
and␈αapply␈α
techniques␈α
for␈αproving␈α
properties␈α
of␈αprograms␈α
manipulating␈α
graphs.␈α The
␈↓ ↓H␈↓proofs should be fully formal, but also natual and cleanly expressible.

␈↓ ↓H␈↓2.␈α Develop␈αthe␈αtheory␈αof␈αre-entrant␈α
list␈αstructures.␈α (see␈αChapter␈αIV.)␈αDecide␈αon␈α
a␈αrepresentation
␈↓ ↓H␈↓of␈α∀such␈α∃structures␈α∀as␈α∀ordinary␈α∃lists␈α∀(say␈α∃with␈α∀pointers␈α∀and␈α∃labels).␈α∀ Define␈α∃some␈α∀primitive
␈↓ ↓H␈↓operations␈α(for␈αexample:␈α␈↓↓car␈αcdr␈αcons␈αpoint␈αcut␈↓).␈α Write␈αprograms␈αto␈αgo␈αfrom␈αone␈αrepresentation␈αto
␈↓ ↓H␈↓the␈α∂other.␈α∂ Write␈α∞an␈α∂equality␈α∂predicate␈α∂in␈α∞for␈α∂structures␈α∂in␈α∞your␈α∂representation.␈α∂  Work␈α∂out␈α∞an
␈↓ ↓H␈↓induction␈α∂schema␈α∂to␈α∞allow␈α∂you␈α∂to␈α∂tell␈α∞when␈α∂programs␈α∂on␈α∞such␈α∂structures␈α∂will␈α∂terminate.␈α∞ Write
␈↓ ↓H␈↓some interesting programs on such structures and prove some facts about them.


␈↓ ↓H␈↓αFormal systems

␈↓ ↓H␈↓3.␈αWrite␈α
a␈αproof␈α
checker␈αfor␈αa␈α
simple␈αformal␈α
system.␈α  Some␈αexamples␈α
of␈αsuitable␈α
formal␈αsystems
␈↓ ↓H␈↓are:

␈↓ ↓H␈↓␈↓ αH3.1. Trigonometric expressions: using trig identities to prove expressions equivalent.
␈↓ ↓H␈↓␈↓ αH3.2.␈αSymbolic␈α
integration:␈αusing␈αvarious␈α
standard␈αtricks␈α
for␈αmanipulating␈αintegrands␈α
into
␈↓ ↓H␈↓␈↓ αHintegrable form.
␈↓ ↓H␈↓␈↓ αH3.3. Propositional logic and a Hilbert or natural deduction style proof system.
␈↓ ↓H␈↓␈↓ αHImplement some heuristics to search for proofs.
␈↓ ↓H␈↓␈↓ αHDerived rules + ability to unwind.
␈↓ ↓H␈↓␈↓ εH␈↓ 92


␈↓ ↓H␈↓αCompiling

␈↓ ↓H␈↓4. Improve the LCOM4 compiler.  Some possibilities are to modify LCOM4 to:

␈↓ ↓H␈↓␈↓ αH4.1. compile  ␈↓↓label.␈↓
␈↓ ↓H␈↓␈↓ αH4.2. handle the ␈↓αprog␈↓ and related features.
␈↓ ↓H␈↓␈↓ αH4.3. handle functions as arguments (as for ␈↓↓mapcar)␈↓ .
␈↓ ↓H␈↓␈↓ αH4.4. recognize iteration and compile it with loops.
␈↓ ↓H␈↓␈↓ αH4.5. produce more efficient arithmetic code.
␈↓ ↓H␈↓␈↓ αH4.6. compile additional features such as "while's" or "do's" etc..

␈↓ ↓H␈↓5. Write a data driven compiler for LISP.

␈↓ ↓H␈↓6.␈α⊂Write␈α⊂a␈α⊂syntax␈α⊂directed␈α⊂compiler␈α⊂for␈α⊂LISP.␈α⊂  Perhaps␈α⊂several␈α⊂passes␈α⊂using␈α⊃an␈α⊂intermediate
␈↓ ↓H␈↓␈↓ αλlanguage would be useful.


␈↓ ↓H␈↓αGames

␈↓ ↓H␈↓7. Write a program to play a game.  Some possible games are:

␈↓ ↓H␈↓␈↓ αH7.1. 3-dimensional Tic Tac Toe (See Chapter II for 2-D version)
␈↓ ↓H␈↓␈↓ αH7.2. Solitare
␈↓ ↓H␈↓␈↓ αH7.3. Mastermind
␈↓ ↓H␈↓␈↓ αH7.4. Otello

␈↓ ↓H␈↓    There␈α∞are␈α
two␈α∞key␈α∞issues␈α
in␈α∞programs␈α∞to␈α
play␈α∞games.␈α∞ One␈α
is␈α∞the␈α∞method␈α
used␈α∞to␈α∞prune␈α
the
␈↓ ↓H␈↓␈↓ αλsearch␈αfor␈αpossible␈αmoves,␈αthe␈αother␈αis␈αdeveloping␈αgood␈αstrategies␈αof␈αchoosing␈αmoves.␈α These
␈↓ ↓H␈↓␈↓ αλissues are of course not independent from one another.

␈↓ ↓H␈↓    Be␈α⊂sure␈α⊂to␈α⊂hold␈α⊂individual␈α⊂test␈α∂runs␈α⊂to␈α⊂a␈α⊂few␈α⊂seconds.␈α⊂ It␈α∂is␈α⊂easy␈α⊂to␈α⊂use␈α⊂large␈α⊂amounts␈α∂of
␈↓ ↓H␈↓␈↓ αλcomputer time in such projects.


␈↓ ↓H␈↓αSome previous projects.

␈↓ ↓H␈↓8. Minimizing finite state machine

␈↓ ↓H␈↓9. Digital Circuit design

␈↓ ↓H␈↓10. LALR parser